Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		not(not(x))	→ x
2:		not(or(x,y))	→ and(not(not(not(x))),not(not(not(y))))
3:		not(and(x,y))	→ or(not(not(not(x))),not(not(not(y))))

There are 12 dependency pairs:


4:		NOT(or(x,y))	→ NOT(not(not(x)))
5:		NOT(or(x,y))	→ NOT(not(x))
6:		NOT(or(x,y))	→ NOT(x)
7:		NOT(or(x,y))	→ NOT(not(not(y)))
8:		NOT(or(x,y))	→ NOT(not(y))
9:		NOT(or(x,y))	→ NOT(y)
10:		NOT(and(x,y))	→ NOT(not(not(x)))
11:		NOT(and(x,y))	→ NOT(not(x))
12:		NOT(and(x,y))	→ NOT(x)
13:		NOT(and(x,y))	→ NOT(not(not(y)))
14:		NOT(and(x,y))	→ NOT(not(y))
15:		NOT(and(x,y))	→ NOT(y)

Consider the SCC {4-15}. The constraints could not be solved.

Tyrolean Termination Tool (0.37 seconds) --- May 3, 2006